g, h:GrpSig, f:InjMonHom(g;h). Inj(|g|;|h|;f) 

latex

Up	groups 1
Definitions of Statement	MonHom(M1,M2), InjMonHom(g;h)
Definitions	True, T, t  T, x:A. B(x), P  Q, SqStable(P), MonHom(M1,M2), InjMonHom(g;h)
Lemmas	grp sig wf, inj mon hom wf, grp car wf, sq stable inject